Nuprl Lemma : eqfun_p_wf
13,42
postcript
pdf
T
:Type,
eq
:(
T
T
). IsEqFun(
T
;
eq
)
latex
Up
rel
1
,
rel
1
Definitions
P
Q
,
P
Q
,
P
&
Q
,
x
f
y
,
P
Q
,
IsEqFun(
T
;
eq
)
,
,
t
T
,
x
:
A
.
B
(
x
)
Lemmas
bool
wf
,
assert
wf
,
iff
wf
origin
T:Type, eq:(T
T
). IsEqFun(T;eq) 
T:Type, eq:(TT). IsEqFun(T;eq) 
Q
Q Q Tx:A. B(x)